forall a: forall b:
forall c: forall d:
forall Q:a->b:
forall R: b->c:
forall S:a->d:
Q;R&S;L:d,c = (Q&S;L:d,b);R